\begin{tabbing}
[$e_{1}$;$e_{2}$]$\sim$([$a$,$b$].$p$($a$;$b$))$\ast$[$a$,$b$].$q$($a$;$b$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$m$:$\mathbb{N}^{+}$\+
\\[0ex]$\exists$\=$f$:int\_seg(0; $m$)$\rightarrow$\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = loc($e_{1}$)\} \+
\\[0ex]((($f$(0) = $e_{1}$) $\wedge$ es{-}le(${\it es}$; ($f$($m$ {-} 1)); $e_{2}$))
\\[0ex]$\wedge$ \=(($\forall$$i$:int\_seg(0; ($m$ {-} 1)). es{-}locl(${\it es}$; ($f$($i$)); ($f$($i$ + 1))))\+
\\[0ex]$\wedge$ ($\forall$$i$:int\_seg(0; ($m$ {-} 1)). $p$($f$($i$);es{-}pred(${\it es}$; ($f$($i$ + 1))))))
\-\\[0ex]$\wedge$ $q$($f$($m$ {-} 1);$e_{2}$))
\-\-
\end{tabbing}